\begin{tabbing}
$\forall$${\it es}$:ES, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $R$:(State(${\it ds}$)$\rightarrow$State(${\it ds}$)$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$s$, ${\it s'}$:State(${\it ds}$). Dec($R$($s$,${\it s'}$)))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:\{$e$:E$\mid$ @loc($e$) discrete ${\it ds}$\} .\+
\\[0ex]$\exists$${\it e'}$$\geq$$e$.$R$((state when $e$),state after ${\it e'}$)
\\[0ex]$\Rightarrow$ $\exists$${\it e'}$$\geq$$e$.\=$R$((state when $e$),state after ${\it e'}$)\+
\\[0ex]\& $\forall$${\it e''}$$\in$[$e$,${\it e'}$).$\neg$($R$((state when $e$),state after ${\it e''}$)))
\-\-
\end{tabbing}